For a long time now, formal methods have been successfully used to analyze security protocols. Several tools have even been developed to tackle automatically different proof techniques and, therefore, to ease the verification of such protocols. However, when it comes to electronic voting and APIs, current tools tend to reach their limits because they can’t handle some cryptographic primitives (e.g. homomorphic encryption), or the security properties (e.g. ballot secrecy), involved in those protocols.In this thesis, we first work on two cases studies of existing and deployed systems: a Norwegian e-voting protocol and a CNRS boardroom voting protocol. These two protocols are analyzed using the applied pi-calculus model and we discuss in details about their security properties, in different corruption scenarios. Even though this part provides several reusable results, it also shows the complexity to prove them by hand and, therefore, underlying a real need for automation in those proofs.The third part of this thesis focuses on a possible lead in direction of this needed automation: type- systems. Indeed, we build upon a recent work describing a new type-system designed to deal with equivalence properties, in order to apply this on the verification of equivalence-based properties in elec- tronic voting like ballot-secrecy. We present an application of this method through the example of Helios, a well-known, web-based, and open-audit, e-voting system.Another family of advanced security protocols are APIs: secure interfaces devoted to allow access to some information stored into a secured trusted hardware without leaking it outside. Such protocols are not immune to attacks; in fact, recent work seems to show the opposite. In the second part of this thesis, we provide a new design for APIs, including a revocation functionality, which is not always considered. In addition, we include a fully formal analysis of this API allowing that a malicious combination of API’s commands does not leak any key, even when the adversary may brute-force some of them.

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000875 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 000875 | SxmlIndent | more

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Exploration
   |type=    RBID
   |clé=     Hal:tel-01107718
   |texte=   Formal Verification of Advanced Families of Security Protocols: E-Voting and APIs
}}